Nuprl Lemma : comb_for_l_all_wf
4,23
postcript
pdf
(
T
,
L
,
P
,
z
.
x
L
.
P
(
x
))
T
:Type
(
T
List)
(
T
Prop)
True
Prop
latex
Definitions
Prop
,
True
,
t
T
,
x
:
A
.
B
(
x
)
,
T
Lemmas
l
all
wf
,
squash
wf
,
true
wf
origin
T,L,P,z. 
x
L. P(x)) T:Type
(T List)(TProp)
TrueProp T,L,P,z. xL. P(x)) T:Type(T List)(TProp)TrueProp Tx:A. B(x)T